ds:x:Id fp Type, da:k:Knd fp Type, es:ES, i:Id, LL:(event-info(ds;da) List) List, e1,
e2:{e:E| loc(e) = i }, L:event-info(ds;da) List.
(LLL. L = nil)
 L = nil
 (x:Id. vartype(i;x)  ds(x)?Top)
 (e:E. loc(e) = i  valtype(e)  da(kind(e))?Top)
 es-hist{i:l}(es;e1;e2) = (concat(LL) @ L)  event-info(ds;da) List
 (f:((||LL||+1){e:E| loc(e) = i }).
 (f(0) = e1 & f(||LL||)  e2 
 (& (i:||LL||. (f(i) <loc f(i+1)))
 (& (i:||LL||. es-hist{i:l}(es;f(i);pred(f(i+1))) = LL[i]  event-info(ds;da) List)
 (& & es-hist{i:l}(es;f(||LL||);e2) = L) 

latex

Definitions	x:A. B(x), t  T, x. t(x), P  Q, as @ bs, concat(ll), x:A. B(x), {i..j}, ||as||, A & B, P & Q, reduce(f;k;as), Y, i  j < k, Prop, P  Q, P  Q, Top, S  T, x(s), A, AB, False, Dec(P), P  Q
Lemmas	event-info wf, Id wf, event system wf, fpf wf, Knd wf, int seg wf, le wf, es-le wf, es-locl wf, es-hist wf, es-E wf, es-loc wf, es-valtype wf, fpf-cap wf, Kind-deq wf, es-kind wf, top wf, es-vartype wf, id-deq wf, not wf, l all wf, decidable es-locl, null-es-hist, assert wf, null wf3, assert of null, es-le-not-locl